
type op_comp = Eq | Lt | Le | Neq
type op_arith = Plus | Minus

type const = ConstInt of int32 | ConstReal of float | ConstName of string

type term = 
  | Const of const
  | Elem of string
  | Access of string * string list
  | Arith of term * op_arith * const

module rec Atom : sig
  type t =
    | True
    | False
    | Comp of term * op_comp * term
    | Ite of SAtom.t * t * t

  val compare : t -> t -> int
end 
and SAtom : Set.S with type elt = Atom.t

module SSAtom : Set.S with type elt = SAtom.t

type update = {
  up_arr : string;
  up_arg : string list;
  up_swts : (SAtom.t * term) list;
}
    
type transition = {
  tr_name : string;
  tr_args : string list;
  tr_reqs : SAtom.t;
  tr_ureq : (string * SAtom.t list) list;
  tr_assigns : (string * term) list;
  tr_arrass : (string * string list * term) list;
  tr_upds : update list;
  tr_nondets : string list
}

type elem = string * (string list)

type decl = Dglobal of string * string | Dconst of string * string
            | Darray of string * (string list * string)

type assign = Avar of string * term | Aarray of string * string list * term
    
type decls =
  | Dlist of decl list
  | Dapp of decls * decls

val nop : decls

val decl_l: decl list -> decls

val (++) : decls -> decls -> decls

type state =
  | Sinit of string option * SAtom.t
  | Sinv of (string list * SAtom.t)
  | Scand of string
  | Sunsafe of (string list * SAtom.t)
  | Sforward of (string list * string list * SAtom.t)
  | Strans of transition

type states =
  | Slist of state list
  | Sapp of states * states

val nost : states

val state_l: state list -> states

val (+++) : states -> states -> states

type qdnf =
  | QDnone of SSAtom.t
  | QDexists of string * SSAtom.t
  | QDforall of string * SSAtom.t
  
type system = {
  num_procs : int;
  type_defs : elem list;
  decls : decls;
  states : states;
}

(* Pretty-printer *)
  
val print_system : Format.formatter -> system -> unit

val print_op_comp : Format.formatter -> op_comp -> unit
val print_const : Format.formatter -> const -> unit
val print_term : Format.formatter -> term -> unit
val print_atom : Format.formatter -> Atom.t -> unit
val print_satom : bool -> Format.formatter -> SAtom.t -> unit
val print_transition : Format.formatter -> transition -> unit
val print_unsafe : Format.formatter -> (string list * SAtom.t) -> unit
val print_inv : Format.formatter -> (string list * SAtom.t) -> unit
val print_init : Format.formatter -> (string option * SAtom.t) -> unit
val print_typedef: Format.formatter -> elem list -> unit
val print_decl : Format.formatter -> decl -> unit
val print_decls : Format.formatter -> decls -> unit
